Program verification systems are tasked with proving that a program performs the actions and objectives the program was written to realize. The definition of what the program is expected to do is often referred to as the program's specification. Most program verification systems transform a program into one or more logical expressions that are then tested for validity against the specification. The logical expression represents the weakest precondition of the program relative to the specification of the program. When the expression is proved, then the program is considered correct.
Automated theorem proving or automatic program verification refers to the proving or refuting of mathematical conjectures by a computer program. Depending on the underlying logic, the problem of deciding the validity of a conjecture varies from trivial to impossible. For automatic program verification, parts of the computer program are translated into verification conditions. Each one of these verification conditions is valid if and only if the program is correct with respect to the properties that being verified. These verification conditions may be passed to a theorem prover that attempts to determine whether or not the verification condition is valid.